package org.eclipse.iota.rules;

import java.util.ArrayList;
import java.util.List;

import org.eclipse.iota.assignments.Assignment;
import org.eclipse.iota.model.Clause;
import org.eclipse.iota.model.Constraint;
import org.eclipse.iota.model.Equation;
import org.eclipse.iota.model.Variable;
import org.eclipse.iota.rewrite.AbstractIotaRule;
import org.eclipse.iota.util.IotaCopyUtil;
import org.eclipse.iota.util.IotaFindUtil;
import org.eclipse.iota.util.IotaVariableSubstituter;
import org.eclipse.iota.util.IotaVariableUtil;

/**
 * @author Christian Krause
 * @generated NOT
 */
public class SubstituteVariables extends AbstractIotaRule {
	
	/*
	 * (non-Javadoc)
	 * @see org.eclipse.iota.rules.AbstractIotaRule#visit(org.eclipse.iota.core.Clause)
	 */
	public void visit(Clause clause) {
		
		// Create a new assignment:
		Assignment assignment = new Assignment();
		for (Constraint constraint : clause.getConstraints()) {
			if (constraint instanceof Equation) {
				assignment.createEntryFromEquation((Equation) constraint);
			}
		}
		
		if (!assignment.isEmpty()) {
			IotaVariableSubstituter substituter = new IotaVariableSubstituter(assignment);
			substitute(clause, substituter);
		}
	}
	
	/*
	 * Helper method.
	 */
	private void substitute(Clause clause, IotaVariableSubstituter substituter) {
		
		// Substitute where possible.
		List<Constraint> constraints = new ArrayList<Constraint>(clause.getConstraints());
		//Assignment test = new Assignment();
		
		for (Constraint constraint : constraints) {
			
			// Must be an equation.
			if (constraint instanceof Equation) {
				Equation equation = (Equation) constraint;
				
				// Check if the variable is used in the equation.
				List<Variable> used = IotaVariableUtil.getUsedVariables(equation);
				used.retainAll(substituter.getAssignmnet().keySet());
				if (!used.isEmpty()) {
					
					// Copy the equation.
					Equation copy = IotaCopyUtil.copy(equation);
					copy.setInferred(true);
					
					// Replace the variable.
					substituter.applyTo(copy);
					
					// Simplify the equation immediately and check monotonicity.
					//IotaEquationSimplifier.simplify(copy);
					// CheckMonotonicity. ...
					
					// Add the new equation to the clause only if it is not there already.
					if (!IotaFindUtil.contains(clause, copy)) {
						clause.getConstraints().add(copy);
					}
					
				}
			}
		}
		
	}
	
}
